/*
 * RMonoidR.h
 *
 *  Created on: May 22, 2012
 *      Author: kobe
 */

#ifndef RMONOIDR_H_
#define RMONOIDR_H_

#include "VariousRule.h"

class R_MonoidR: public VariousRule {
public:
	R_MonoidR();
	virtual ~R_MonoidR();
	std::vector<Sequent*> run(Sequent*);
	std::vector<Sequent*> run(Sequent*, size_t);
	std::string toString();
	std::string toLatex();
private:
	Context* search(Context*);
	Sequent* mCurrentSequent;
};

#endif /* RMONOIDR_H_ */
